package bcontractor.base;

import bcontractor.api.SATReasoner;
import bcontractor.api.Sentence;
import bcontractor.api.SentenceSet;

/**
 * A reasoner that delegates it's work to another and keeps track of the number of times it was used.
 * 
 * @author lundberg
 * 
 * @param <S>
 */
public class CountingReasoner<S extends Sentence<S>> implements SATReasoner<S> {

	private final SATReasoner<S> delegate;

	private int count = 0;

	private long timeSpent = 0;

	private long start = 0;

	/**
	 * Constructor
	 * 
	 * @param delegate delegate
	 */
	public CountingReasoner(SATReasoner<S> delegate) {
		this.delegate = delegate;
	}

	/**
	 * {@inheritDoc}
	 */
	@Override
	public boolean entails(SentenceSet<S> sentences, S sentence) {
		start();
		try {
			return delegate.entails(sentences, sentence);
		} finally {
			end();
		}
	}

	private void start() {
		count++;
		start = System.currentTimeMillis();
	}

	private void end() {
		timeSpent += System.currentTimeMillis() - start;
	}

	/**
	 * {@inheritDoc}
	 */
	@Override
	public boolean isUnsatisfiable(SentenceSet<S> sentences) {
		start();
		try {
			return delegate.isUnsatisfiable(sentences);
		} finally {
			end();
		}
	}

	/**
	 * {@inheritDoc}
	 */
	@Override
	public boolean isSatisfiable(SentenceSet<S> sentences) {
		start();
		try {
			return delegate.isSatisfiable(sentences);
		} finally {
			end();
		}
	}

	public int getCount() {
		return count;
	}

	public long getTimeSpent() {
		return timeSpent;
	}
}
